All four people start out on the southern side of the bridge, namely the King, Queen, a young Lady and a Knight. The goal is for everyone to arrive at the castle- the north of the bridge, before the time runs out. The bridge can hold at most two people at a time and they must be carrying the torch when crossing the bridge. The King needs 5 minutes to cross, the Queen 10 minutes, the Lady 2 minutes and the Knight 1 minute. The question is given a specific amount of time, whether all people can cross the bridge in time.

The parital declaration part
////////////////The Model//////////////////
#define Max 17;

#define KNIGHT 1;
#define LADY 2;
#define KING 5;
#define QUEEN 10;

var Knight: {0..1} = 0;
var Lady: {0..1} = 0;
var King: {0..1}= 0;
var Queen: {0..1} = 0;
var time: {0..17} = 0;

The declaration includes some definitions of the constants in this model, where #define  is a reserved keyword for defining a synonymy for a (integer or Boolean) constant or a proposition.  Max represents the maximum number of time units. KNIGHT stands for the number of time units the knight needs. Similarly, we define the rest ones.  We remark the users shall use constants (instead of variables) whenever possible. Because constants never change, during verification they are not excluded from the system state information, and hence, using constants instead of variables save memory and maybe time also.

The above also defines the variables in the system, where var is a reserved keyword for introducing variables or arrays. Notice that PAT has a weak type system. Variable Knight is used to model whether the knight is at the southern side of the bridge or the northern side. It is of value 0 if the knight hasn't crossed the bridge, otherwise 1. Similarly, we define the rest. Variable time records the number of time units spent by far. The default value is 0.  The two numbers between "{}" is the lower bound and upper bound values of the variable. When user selectd the BDD selection in the Verification Dialog, these numbers are very helpful to the program to calculate the number of bits needed to represent that variable.

The process P1 has two states North and South. Each transtion from North to South corresponds the case when someone go from North to South and vice versa. The label of the transition is in the following form:

[guard]event{program}

Informally, it means that if the guard is true, then the action can occur, i.e., the program attached with the action can be executed. Notice that program here could contain while-loops, if-then-else, etc. For instance, at the first line, the guard states that the Knight and the Lady  are both at the southern side of the bridge. If this is true, then the action go_knight_lady can occur, which in terms means that the variable Knight and Lady are set to be 1 (meaning they have crossed the bridge) and time is incremented by the number of time units needed by the lady. After that, the system behaves as process North because the torch must come back from North to South. Similarly, we can enumerate all possible ways of crossing the bridge, e.g., the knight goes together with the king or queen, the king goes with the lady or queen, and the queen goes with the lady.

Having modeled all possible behaviors of the systems as the above processes, we are now ready to reason about the system. 

The rest of the declaration part
System = P1();
#define goal (Knight==1 && Lady==1 && King==1 && Queen==1 && time <= Max);
#assert System reaches goal;

The question we are interested is whether it is feasible to cross the bridge within Max number of time unit. The above shows one of the questions. The first line defines that the system only includes the process P1. The second line defines a proposition named goal, which states that the time taken should be not greater than Max and all people should be on the northern side of the bridge. The third line is the assertion, where #assert is a reserved keyword.  'reaches' is also a keyword. Informally, the assertion says that starting from process South() (because the state South is the initial state of the process P1), we will reach a state at which the proposition goal is true.